package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.ClockGuard;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.SimpleClockGuard;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class Radar {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("Radar");
		 
		 // Clocks and their guards
		 
		 tiosts.addClock("clock3");			 	 
		 
         // Variables
         TypedData modeR = new TypedData("modeR", Constants.TYPE_INTEGER);
         tiosts.addVariable(modeR);
         TypedData terrainView = new TypedData("terrainView", Constants.TYPE_INTEGER);
         tiosts.addVariable(terrainView);
         TypedData rangeContacts = new TypedData("rangeContacts", Constants.TYPE_INTEGER);
         tiosts.addVariable(rangeContacts);
         TypedData contactID = new TypedData("contactID", Constants.TYPE_INTEGER);
         tiosts.addVariable(contactID);         
         TypedData rangeR = new TypedData("rangeR", Constants.TYPE_INTEGER);
         tiosts.addVariable(rangeR);
         TypedData azimuthR = new TypedData("azimuthR", Constants.TYPE_INTEGER);
         tiosts.addVariable(azimuthR);
         TypedData elevationR = new TypedData("elevationR", Constants.TYPE_INTEGER);
         tiosts.addVariable(elevationR);
         
         // Parameters
         TypedData op = new TypedData("op", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(op);
         TypedData info = new TypedData("info", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(info);
         TypedData value = new TypedData("value", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(value);   
         TypedData id = new TypedData("id", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(id);
         TypedData r = new TypedData("r", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(r);
         TypedData a = new TypedData("a", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(a);
         TypedData e = new TypedData("e", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(e);
         
         // Input, output, and internal actions
         Action init = new Action("init3", Constants.ACTION_INTERNAL);
         tiosts.addAction(init);
    
         Action selectR = new Action("selectR", Constants.ACTION_INPUT);
         selectR.addParameter(op.getName());
         tiosts.addAction(selectR);
         
         Action receive = new Action("receive", Constants.ACTION_INPUT);
         receive.addParameter(info.getName());
         tiosts.addAction(receive);
         
         Action display = new Action("display", Constants.ACTION_OUTPUT);
         display.addParameter(info.getName());
         tiosts.addAction(display);
         
         Action range = new Action("range", Constants.ACTION_INPUT);
         range.addParameter(value.getName());
         tiosts.addAction(range);
         
         Action detect = new Action("detect", Constants.ACTION_INPUT);
         detect.addParameter(value.getName());
         tiosts.addAction(detect);
         
         Action targetPosition = new Action("targetPosition", Constants.ACTION_INPUT);
         targetPosition.addParameter(r.getName());
         targetPosition.addParameter(a.getName());
         targetPosition.addParameter(e.getName());
         tiosts.addAction(targetPosition);
         
         Action track = new Action("track", Constants.ACTION_INPUT);
         track.addParameter(id.getName());
         tiosts.addAction(track);       
                           
         // Locations
         Location start = new Location("Start3");
         tiosts.addLocation(start);
         Location S36 = new Location("S36");
         tiosts.addLocation(S36);
         Location S37 = new Location("S37");
         tiosts.addLocation(S37);     
         Location S38 = new Location("S38");
         tiosts.addLocation(S38);
         Location S39 = new Location("S39");
         tiosts.addLocation(S39); 
         Location S40 = new Location("S40");
         tiosts.addLocation(S40); 
         Location S41 = new Location("S41");
         tiosts.addLocation(S41);  
         
         // Initial Condition
         tiosts.setInitialCondition(Constants.GUARD_TRUE);
         
         // Initial Location
         tiosts.setInitialLocation(start);
         
         // Transitions
         tiosts.createTransition("Start3", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init, null, null, "S36");
         tiosts.createTransition("S36", Constants.GUARD_TRUE, Constants.GUARD_TRUE, selectR, "modeR := op", "clock3 := 0", "S37");
         //groundMap assumes 4
         tiosts.createTransition("S37", "modeR = 4", Constants.GUARD_TRUE, receive, "terrainView := info", null, "S38");
         //terrainView assumes 5
         tiosts.createTransition("S38", "info = 5", Constants.GUARD_TRUE, display, null, null, "S36");
         //groundSearch assumes 6
         tiosts.createTransition("S37", "modeR = 6", Constants.GUARD_TRUE, range, "rangeContacts := value", null, "S39");
         tiosts.createTransition("S39", "rangeContacts > 10", "clock3 <= 82", detect, "rangeContacts := 10| contactID := value", null, "S40");
         tiosts.createTransition("S40", Constants.GUARD_TRUE, Constants.GUARD_TRUE, targetPosition, "rangeR := r AND azimuthR := a AND elevationR := e", null, "S41");
         tiosts.createTransition("S41", Constants.GUARD_TRUE, Constants.GUARD_TRUE, track, "contactID := id", null, "S36");
         
         return tiosts;		 
	 }

}
